g:IAbMonoid, a, b:.
(a  b)
 (E, F:({a..b}|g|).
 ( a  i < b. E(i) * F(i)) = (( a  i < b. E(i)) * ( a  i < b. F(i)))  |g|) 

latex

Up	groups 1
Definitions of Statement	IMonoid, IAbMonoid
Definitions	t  T, x:A. B(x), x. t(x), {T}, , x(s), x f y, P  Q, P & Q, P  Q, P  Q, False, A, A  B, i  j < k, {i..j}, IMonoid, {i...}, IAbMonoid
Lemmas	iabmonoid wf, int upper wf, grp op wf, mon itop wf, grp car wf, int seg wf, int le to int upper, int upper ind, mon ident, grp id wf, mon itop unroll base, mon itop unroll hi, abmonoid ac 1, mon assoc, le wf